Iof proof for Lemma fun with inv is bij:
1. A : Type
2. B : Type
3. f : A
B
4. g : B
A
5. (g o f) = Id{A}
6. (f o g) = Id{B}
7. a1 : A
8. a2 : A
9. f(a1) = f(a2)
10. g(f(a1)) = g(f(a2))
a1 = a2
by ((((NotThinning (With a1 (EqHD 5)))
CollapseTHENM (With a2 (EqHD 5)))
)
CollapseTHENA (
C(Auto_aux (first_nat 1:n) ((first_nat 1:n),(first_nat 4:n)) (first_tok :t) inil_term)))
C1:
C1: 5. (f o g) = Id{B}
C1: 6. a1 : A
C1: 7. a2 : A
C1: 8. f(a1) = f(a2)
C1: 9. g(f(a1)) = g(f(a2))
C1: 10. (g o f)(a1) = Id{A}(a1)
C1: 11. (g o f)(a2) = Id{A}(a2)
C1: a1 = a2
C.